YES 1.587 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/empty.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ BR

mainModule Main
  ((elem :: Eq a => Maybe a  ->  [Maybe a ->  Bool) :: Eq a => Maybe a  ->  [Maybe a ->  Bool)

module Main where
  import qualified Prelude



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ BR
HASKELL
      ↳ COR

mainModule Main
  ((elem :: Eq a => Maybe a  ->  [Maybe a ->  Bool) :: Eq a => Maybe a  ->  [Maybe a ->  Bool)

module Main where
  import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
HASKELL
          ↳ Narrow

mainModule Main
  (elem :: Eq a => Maybe a  ->  [Maybe a ->  Bool)

module Main where
  import qualified Prelude



Haskell To QDPs


↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(xv2400), Succ(xv4000000)) → new_primPlusNat(xv2400, xv4000000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(xv30000), Succ(xv400000)) → new_primMulNat(xv30000, Succ(xv400000))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(xv3000), Succ(xv40000)) → new_primEqNat(xv3000, xv40000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof
              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(app(ty_@2, ba), bb), bc) → new_esEs(xv300, xv4000, ba, bb)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(ty_[], bd), bc) → new_esEs0(xv300, xv4000, bd)
new_esEs3(Just(@2(xv300, xv301)), Just(@2(xv4000, xv4001)), app(app(ty_@2, cc), app(app(ty_Either, cg), da))) → new_esEs1(xv301, xv4001, cg, da)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(app(app(ty_@3, bad), bae), baf)), hg), hh)) → new_esEs2(xv300, xv4000, bad, bae, baf)
new_esEs1(Right(xv300), Right(xv4000), gc, app(ty_Maybe, hd)) → new_esEs3(xv300, xv4000, hd)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, hg, app(ty_[], bcd)) → new_esEs0(xv302, xv4002, bcd)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, bah), hg), app(app(ty_Either, bce), bcf))) → new_esEs1(xv302, xv4002, bce, bcf)
new_esEs1(Left(xv300), Left(xv4000), app(ty_[], fc), fb) → new_esEs0(xv300, xv4000, fc)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(ty_Maybe, cb), bc) → new_esEs3(xv300, xv4000, cb)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, hg, app(ty_Maybe, bdb)) → new_esEs3(xv302, xv4002, bdb)
new_esEs3(Just(Left(xv300)), Just(Left(xv4000)), app(app(ty_Either, app(app(ty_Either, fd), ff)), fb)) → new_esEs1(xv300, xv4000, fd, ff)
new_esEs1(Left(xv300), Left(xv4000), app(app(ty_Either, fd), ff), fb) → new_esEs1(xv300, xv4000, fd, ff)
new_esEs3(Just(@2(xv300, xv301)), Just(@2(xv4000, xv4001)), app(app(ty_@2, app(app(app(ty_@3, bg), bh), ca)), bc)) → new_esEs2(xv300, xv4000, bg, bh, ca)
new_esEs3(Just(:(xv300, xv301)), Just(:(xv4000, xv4001)), app(ty_[], app(ty_[], dh))) → new_esEs0(xv300, xv4000, dh)
new_esEs3(Just(Right(xv300)), Just(Right(xv4000)), app(app(ty_Either, gc), app(ty_[], gf))) → new_esEs0(xv300, xv4000, gf)
new_esEs1(Right(xv300), Right(xv4000), gc, app(app(ty_@2, gd), ge)) → new_esEs(xv300, xv4000, gd, ge)
new_esEs3(Just(Right(xv300)), Just(Right(xv4000)), app(app(ty_Either, gc), app(app(ty_Either, gg), gh))) → new_esEs1(xv300, xv4000, gg, gh)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(app(ty_@2, he), hf)), hg), hh)) → new_esEs(xv300, xv4000, he, hf)
new_esEs3(Just(Left(xv300)), Just(Left(xv4000)), app(app(ty_Either, app(app(ty_@2, eh), fa)), fb)) → new_esEs(xv300, xv4000, eh, fa)
new_esEs3(Just(@2(xv300, xv301)), Just(@2(xv4000, xv4001)), app(app(ty_@2, app(ty_Maybe, cb)), bc)) → new_esEs3(xv300, xv4000, cb)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), cc, app(app(ty_Either, cg), da)) → new_esEs1(xv301, xv4001, cg, da)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), cc, app(ty_[], cf)) → new_esEs0(xv301, xv4001, cf)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), cc, app(app(ty_@2, cd), ce)) → new_esEs(xv301, xv4001, cd, ce)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, bah), hg), app(ty_[], bcd))) → new_esEs0(xv302, xv4002, bcd)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(app(app(ty_@3, bg), bh), ca), bc) → new_esEs2(xv300, xv4000, bg, bh, ca)
new_esEs1(Left(xv300), Left(xv4000), app(ty_Maybe, gb), fb) → new_esEs3(xv300, xv4000, gb)
new_esEs1(Left(xv300), Left(xv4000), app(app(ty_@2, eh), fa), fb) → new_esEs(xv300, xv4000, eh, fa)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_@2, he), hf), hg, hh) → new_esEs(xv300, xv4000, he, hf)
new_esEs3(Just(@2(xv300, xv301)), Just(@2(xv4000, xv4001)), app(app(ty_@2, app(app(ty_Either, be), bf)), bc)) → new_esEs1(xv300, xv4000, be, bf)
new_esEs3(Just(Left(xv300)), Just(Left(xv4000)), app(app(ty_Either, app(ty_[], fc)), fb)) → new_esEs0(xv300, xv4000, fc)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_[], baa), hg, hh) → new_esEs0(xv300, xv4000, baa)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, bah), hg), app(app(app(ty_@3, bcg), bch), bda))) → new_esEs2(xv302, xv4002, bcg, bch, bda)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, app(ty_[], bbc), hh) → new_esEs0(xv301, xv4001, bbc)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, bah), hg), app(app(ty_@2, bcb), bcc))) → new_esEs(xv302, xv4002, bcb, bcc)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(ty_[], baa)), hg), hh)) → new_esEs0(xv300, xv4000, baa)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), app(app(ty_Either, be), bf), bc) → new_esEs1(xv300, xv4000, be, bf)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, bah), app(app(ty_Either, bbd), bbe)), hh)) → new_esEs1(xv301, xv4001, bbd, bbe)
new_esEs0(:(xv300, xv301), :(xv4000, xv4001), eg) → new_esEs0(xv301, xv4001, eg)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, hg, app(app(app(ty_@3, bcg), bch), bda)) → new_esEs2(xv302, xv4002, bcg, bch, bda)
new_esEs3(Just(Left(xv300)), Just(Left(xv4000)), app(app(ty_Either, app(app(app(ty_@3, fg), fh), ga)), fb)) → new_esEs2(xv300, xv4000, fg, fh, ga)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, hg, app(app(ty_Either, bce), bcf)) → new_esEs1(xv302, xv4002, bce, bcf)
new_esEs3(Just(@2(xv300, xv301)), Just(@2(xv4000, xv4001)), app(app(ty_@2, cc), app(app(app(ty_@3, db), dc), dd))) → new_esEs2(xv301, xv4001, db, dc, dd)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(app(ty_@3, bad), bae), baf), hg, hh) → new_esEs2(xv300, xv4000, bad, bae, baf)
new_esEs0(:(xv300, xv301), :(xv4000, xv4001), app(ty_Maybe, ef)) → new_esEs3(xv300, xv4000, ef)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(ty_Maybe, bag)), hg), hh)) → new_esEs3(xv300, xv4000, bag)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, app(ty_Maybe, bca), hh) → new_esEs3(xv301, xv4001, bca)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, bah), app(app(ty_@2, bba), bbb)), hh)) → new_esEs(xv301, xv4001, bba, bbb)
new_esEs3(Just(@2(xv300, xv301)), Just(@2(xv4000, xv4001)), app(app(ty_@2, cc), app(ty_Maybe, de))) → new_esEs3(xv301, xv4001, de)
new_esEs3(Just(:(xv300, xv301)), Just(:(xv4000, xv4001)), app(ty_[], app(app(ty_@2, df), dg))) → new_esEs(xv300, xv4000, df, dg)
new_esEs0(:(xv300, xv301), :(xv4000, xv4001), app(app(app(ty_@3, ec), ed), ee)) → new_esEs2(xv300, xv4000, ec, ed, ee)
new_esEs1(Right(xv300), Right(xv4000), gc, app(ty_[], gf)) → new_esEs0(xv300, xv4000, gf)
new_esEs1(Right(xv300), Right(xv4000), gc, app(app(ty_Either, gg), gh)) → new_esEs1(xv300, xv4000, gg, gh)
new_esEs3(Just(:(xv300, xv301)), Just(:(xv4000, xv4001)), app(ty_[], app(ty_Maybe, ef))) → new_esEs3(xv300, xv4000, ef)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), cc, app(ty_Maybe, de)) → new_esEs3(xv301, xv4001, de)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, bah), app(ty_Maybe, bca)), hh)) → new_esEs3(xv301, xv4001, bca)
new_esEs(@2(xv300, xv301), @2(xv4000, xv4001), cc, app(app(app(ty_@3, db), dc), dd)) → new_esEs2(xv301, xv4001, db, dc, dd)
new_esEs3(Just(Left(xv300)), Just(Left(xv4000)), app(app(ty_Either, app(ty_Maybe, gb)), fb)) → new_esEs3(xv300, xv4000, gb)
new_esEs3(Just(@2(xv300, xv301)), Just(@2(xv4000, xv4001)), app(app(ty_@2, cc), app(app(ty_@2, cd), ce))) → new_esEs(xv301, xv4001, cd, ce)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, app(app(ty_Either, bbd), bbe), hh) → new_esEs1(xv301, xv4001, bbd, bbe)
new_esEs1(Left(xv300), Left(xv4000), app(app(app(ty_@3, fg), fh), ga), fb) → new_esEs2(xv300, xv4000, fg, fh, ga)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, bah), app(ty_[], bbc)), hh)) → new_esEs0(xv301, xv4001, bbc)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, bah), hg), app(ty_Maybe, bdb))) → new_esEs3(xv302, xv4002, bdb)
new_esEs1(Right(xv300), Right(xv4000), gc, app(app(app(ty_@3, ha), hb), hc)) → new_esEs2(xv300, xv4000, ha, hb, hc)
new_esEs3(Just(Right(xv300)), Just(Right(xv4000)), app(app(ty_Either, gc), app(app(app(ty_@3, ha), hb), hc))) → new_esEs2(xv300, xv4000, ha, hb, hc)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, app(app(app(ty_@3, bbf), bbg), bbh), hh) → new_esEs2(xv301, xv4001, bbf, bbg, bbh)
new_esEs3(Just(xv30), Just(xv400), app(ty_Maybe, bdc)) → new_esEs3(xv30, xv400, bdc)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(ty_Maybe, bag), hg, hh) → new_esEs3(xv300, xv4000, bag)
new_esEs0(:(xv300, xv301), :(xv4000, xv4001), app(app(ty_Either, ea), eb)) → new_esEs1(xv300, xv4000, ea, eb)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), app(app(ty_Either, bab), bac), hg, hh) → new_esEs1(xv300, xv4000, bab, bac)
new_esEs3(Just(Right(xv300)), Just(Right(xv4000)), app(app(ty_Either, gc), app(ty_Maybe, hd))) → new_esEs3(xv300, xv4000, hd)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, app(app(ty_Either, bab), bac)), hg), hh)) → new_esEs1(xv300, xv4000, bab, bac)
new_esEs0(:(xv300, xv301), :(xv4000, xv4001), app(app(ty_@2, df), dg)) → new_esEs(xv300, xv4000, df, dg)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, app(app(ty_@2, bba), bbb), hh) → new_esEs(xv301, xv4001, bba, bbb)
new_esEs3(Just(Right(xv300)), Just(Right(xv4000)), app(app(ty_Either, gc), app(app(ty_@2, gd), ge))) → new_esEs(xv300, xv4000, gd, ge)
new_esEs3(Just(@3(xv300, xv301, xv302)), Just(@3(xv4000, xv4001, xv4002)), app(app(app(ty_@3, bah), app(app(app(ty_@3, bbf), bbg), bbh)), hh)) → new_esEs2(xv301, xv4001, bbf, bbg, bbh)
new_esEs3(Just(@2(xv300, xv301)), Just(@2(xv4000, xv4001)), app(app(ty_@2, app(app(ty_@2, ba), bb)), bc)) → new_esEs(xv300, xv4000, ba, bb)
new_esEs0(:(xv300, xv301), :(xv4000, xv4001), app(ty_[], dh)) → new_esEs0(xv300, xv4000, dh)
new_esEs3(Just(:(xv300, xv301)), Just(:(xv4000, xv4001)), app(ty_[], eg)) → new_esEs0(xv301, xv4001, eg)
new_esEs2(@3(xv300, xv301, xv302), @3(xv4000, xv4001, xv4002), bah, hg, app(app(ty_@2, bcb), bcc)) → new_esEs(xv302, xv4002, bcb, bcc)
new_esEs3(Just(:(xv300, xv301)), Just(:(xv4000, xv4001)), app(ty_[], app(app(app(ty_@3, ec), ed), ee))) → new_esEs2(xv300, xv4000, ec, ed, ee)
new_esEs3(Just(@2(xv300, xv301)), Just(@2(xv4000, xv4001)), app(app(ty_@2, app(ty_[], bd)), bc)) → new_esEs0(xv300, xv4000, bd)
new_esEs3(Just(@2(xv300, xv301)), Just(@2(xv4000, xv4001)), app(app(ty_@2, cc), app(ty_[], cf))) → new_esEs0(xv301, xv4001, cf)
new_esEs3(Just(:(xv300, xv301)), Just(:(xv4000, xv4001)), app(ty_[], app(app(ty_Either, ea), eb))) → new_esEs1(xv300, xv4000, ea, eb)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ BR
    ↳ HASKELL
      ↳ COR
        ↳ HASKELL
          ↳ Narrow
            ↳ AND
              ↳ QDP
              ↳ QDP
              ↳ QDP
              ↳ QDP
QDP
                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldr(xv3, :(xv40, xv41), ba) → new_foldr(xv3, xv41, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: